Inference at * 2 0 1 2 
Iof proof for Lemma multiply nat wf:

.....basecase..... NILNIL

1. i : 
  (0  0 )  (0  (i * 0)) 

latex

 by D 0 

latex

 1: 

 1: 2. 0  0 
 1:   0  (i * 0)
 2: .....wf..... NILNIL

 2:   (0  0 )  
 .

Definitions	Type, s = t, n * m, #$n, , A  B, x:AB(x), i  j , P  Q, t  T,
Lemmas	le wf, ge wf